//
// Created by xux on 2024/9/11.
//

#pragma once
#ifndef CL4AF_CLAUSE_H
#define CL4AF_CLAUSE_H

#include <vector>
#include <list>
#include <cassert>
#include <unordered_set>

#include "label_lib.h"
#include "Bitset.h"

class Clause {
public:
    std::vector<int>    lit;
    int lbd = 0;

    // 默认构造函数
    Clause() = default;
    // 拷贝构造函数
    Clause(const Clause& other) = default;
    std::vector<int> exclude_as_vector(int arg);
    int get_arg(int index);
    int get_sign(int index);
    void swap(int index1, int index2);
    std::list<int> collect_arg_as_list();
    void update_lbd(std::vector<int> depth);

    int size() const{return (int)lit.size();}
    auto begin(){return lit.begin();}
    auto end(){return lit.end();}

    class ClauseBuilder{
        std::vector<int>    lit;
    public:
        Clause build(const std::vector<int>& depth);
        void add(int arg, int label);
    };
};


#endif //CL4AF_CLAUSE_H
